the_w:World, l:IdLnk, t, t':. match(l;t;t')   

latex

Definitions	P  Q, Msg(M), S  T, Id, source(l), mlnk(m), w.M, match(l;t;t'), p  q, ij, Msg, snds(l;t), Action(i), destination(l), rcvs(l;t), i<j, x:A. B(x), ||as||, onlnk(l;mss), m(i;t), , IdLnk, t  T, World
Lemmas	world wf, IdLnk wf, nat wf, lt int wf, w-rcvs wf, ldst wf, w-action wf, length wf1, w-snds wf, w-Msg wf, le int wf, band wf, mlnk wf, lsrc wf, Id wf, w-onlnk wf, w-M wf, Msg wf, w-m wf